{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "%install_ext https://raw.github.com/cjdrake/ipython-magic/master/gvmagic.py"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "%load_ext gvmagic"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "from pyeda.inter import *"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Abstract"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This paper introduces PyEDA, a Python library for electronic design automation (EDA). PyEDA provides both a high level interface to the representation of Boolean functions,\n",
    "and blazingly-fast C extensions for fundamental algorithms where performance is essential.\n",
    "PyEDA is a hobby project which has the simple but audacious goal of improving the state of digital design by using Python."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Introduction"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Chip design and verification is a complicated undertaking.\n",
    "You must assemble a large team of engineers with many different specialties:\n",
    "front-end design entry, logic verification, power optimization, synthesis,\n",
    "place and route, physical verification, and so on.\n",
    "Unfortunately, the tools, languages,\n",
    "and work flows offered by the electronic design automation (EDA) industry are,\n",
    "in this author's opinion, largely a pit of despair.\n",
    "The languages most familiar to chip design and verification engineers are\n",
    "Verilog (now SystemVerilog), C/C++, TCL, and Perl.\n",
    "Flows are patched together from several proprietary tools with incompatible\n",
    "data representations.\n",
    "Even with Python's strength in scientific computing,\n",
    "it has largely failed to penetrate this space.\n",
    "In short, EDA needs more Python!\n",
    "\n",
    "This paper surveys some of the features and applications of\n",
    "[PyEDA](https://github.com/cjdrake/pyeda),\n",
    "a Python library for electronic design automation.\n",
    "PyEDA provides both a high level interface to the representation of Boolean functions,\n",
    "and blazingly-fast C extensions for fundamental algorithms where\n",
    "performance is essential.\n",
    "\n",
    "PyEDA is a hobby project,\n",
    "but in the past year it has seen some interesting adoption from\n",
    "University students.\n",
    "For example,\n",
    "students at Vanderbilt University used it to model system reliability,\n",
    "and students at Saarland University used as part of a fast DQBF Refutation tool.\n",
    "\n",
    "Even though the name \"PyEDA\" implies that the library is specific to EDA,\n",
    "it is actually general in nature.\n",
    "Some of the techniques used for designing and verifying digital logic are\n",
    "fundamental to computer science.\n",
    "For example, we will discuss applications of Boolean satisfiability (SAT),\n",
    "the definitive NP-complete problem.\n",
    "\n",
    "PyEDA's repository is hosted at https://github.com/cjdrake/pyeda,\n",
    "and its documentation is hosted at http://pyeda.rtfd.org."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Boolean Variables and Functions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "At its core, PyEDA provides a powerful API for creating and\n",
    "manipulating Boolean functions.\n",
    "\n",
    "First, let us provide the standard definitions.\n",
    "\n",
    "A Boolean *variable* is an abstract numerical quantity that can take any\n",
    "value in the set $\\{0, 1\\}$.\n",
    "\n",
    "A Boolean function is a rule that maps points in an $N$-dimensional\n",
    "Boolean space to an element in $\\{0, 1\\}$.\n",
    "Formally, $f: B^N \\Rightarrow B$,\n",
    "where $B^N$ means the Cartesian product of $N$ sets of type $\\{0, 1\\}$.\n",
    "For example, if you have three input variables, $a, b, c$,\n",
    "each defined on $\\{0, 1\\}$,\n",
    "then $B^3 = \\{0, 1\\}^3 = \\{(0, 0, 0), (0, 0, 1), ..., (1, 1, 1)\\}$.\n",
    "$B^3$ is the **domain** of the function (the input part),\n",
    "and $B = \\{0, 1\\}$ is the **range** of the function (the output part).\n",
    "The set of all input variables a function depends on is called its *support*.\n",
    "\n",
    "There are several ways to represent a Boolean function,\n",
    "and different data structures have different tradeoffs.\n",
    "In the following sections,\n",
    "we will give a brief overview of PyEDA's API for logic expressions,\n",
    "truth tables, and binary decision diagrams.\n",
    "In addition,\n",
    "we will provide implementation notes for several useful applications."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Logic Expressions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Logic expressions are a powerful and flexible way to represent Boolean functions.\n",
    "They are implemented as a graph,\n",
    "with *atoms* at the branches, and *operators* at the leaves.\n",
    "Atomic elements are *literals* (variables and complemented variables),\n",
    "and *constants* (zero and one).\n",
    "The supported algebraic operators are `Not`, `Or`, `And`, `Xor`,\n",
    "`Equal`, `Implies`, and `ITE` (if-then-else).\n",
    "\n",
    "For general purpose use,\n",
    "symbolic logic expressions are PyEDA's central data type.\n",
    "Since release ``0.27``,\n",
    "they have been implemented using a high performance C library.\n",
    "\n",
    "Expressions are fast, and reasonably compact.\n",
    "On the other hand, they are generally not canonical,\n",
    "and determining expression equivalence is NP-complete.\n",
    "Conversion to a canonical expression form can result in exponential size."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Construction"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To construct a logic expression, first start by defining some symbolic\n",
    "*variables* of type `Expression`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "a, b, c, d = map(exprvar, 'abcd')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "By overloading Python's logical operators,\n",
    "you can build expression algebraically:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "F = a | ~b & c ^ ~d"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Use methods from the ``Function`` base class to explore the function's\n",
    "basic properties:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F.support"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "list (F.iter_relation())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "There are also several factory functions that offer more power than Python's\n",
    "built-in binary operators.\n",
    "For example, operators such as `Or`, `And`, and `Xor` allow you to\n",
    "construct N-ary expressions:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "a ^ b ^ c"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "Xor(a, b, c)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Also, functions such as `OneHot`, and `Majority`\n",
    "implement powerful, higher order functions:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "OneHot(a, b, c)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "Majority(a, b, c)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Simplification"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The laws of Boolean Algebra can be used to simplify expressions.\n",
    "For example, this table enumerates a partial list of Boolean identities\n",
    "for the `Or` and `And` operators."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "| Name          | OR              | AND                     |\n",
    "|:-------------:|:---------------:|:-----------------------:|\n",
    "| Commutativity | $x + y = y + x$ | $x \\cdot y = y \\cdot x$ |\n",
    "| Associativity | $x + (y + z) = (x + y) + z$ | $x \\cdot (y \\cdot z) = (x \\cdot y) \\cdot z$ |\n",
    "| Identity      | $x + 0 = x$     | $x \\cdot 1 = x$  |\n",
    "| Domination    | $x + 1 = 1$     | $x \\cdot 0 = 0$  |\n",
    "| Idempotence   | $x + x = x$     | $x \\cdot x = x$  |\n",
    "| Inverse       | $x + x' = 1$    | $x \\cdot x' = 0$ |"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Most laws are computationally easy to apply.\n",
    "PyEDA allows you to construct unsimplified Boolean expressions,\n",
    "and provides the `simplify` method to perform such inexpensive\n",
    "transformations."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "For example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F = ~a | a\n",
    "F"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F.simplify()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "Xor(a, ~b, Xnor(~a, b), c)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Performing simplification can dramatically reduce the size and depth of\n",
    "your logic expressions."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Transformation"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "PyEDA also supports a growing list of expression transformations.\n",
    "Since expressions are not a canonical form,\n",
    "transformations can help explore tradeoffs in time and space,\n",
    "as well as convert an expression to a form suitable for a particular algorithm."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "For example,\n",
    "in addition to the primary operators `Not`, `Or`, and `And`,\n",
    "expressions also natively support the secondary `Xor`, `Equal`,\n",
    "`Implies`, and `ITE` (if-then-else) operators.\n",
    "By transforming all secondary operators into primary operators,\n",
    "and pushing all `Not` operators down towards the leaf nodes,\n",
    "you arrive at what is known as \"negation normal form\"."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F = Xor(a >> b, c.eq(d))\n",
    "F.to_nnf()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Currently, expressions also support conversion to the following forms:\n",
    "\n",
    "* Binary operator (only two args per `Or`, `And`, etc)\n",
    "* Disjunctive Normal Form (DNF)\n",
    "* Conjunctive Normal Form (CNF)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "DNF and CNF expressions are \"two-level\" forms.\n",
    "That is, the entire expression is either an `Or` of `And` clauses (DNF),\n",
    "or an `And` of `Or` clauses (CNF).\n",
    "DNF expressions are also called \"covers\",\n",
    "and are important in both two-level and multi-level logic minimization.\n",
    "CNF expressions play an important role in satisfiability.\n",
    "We will briefly cover both of these topics in subsequent sections."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Visualizaton"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Boolean expressions support a `to_dot()` method,\n",
    "which can be used to convert the graph structure to DOT format\n",
    "for consumption by Graphviz.\n",
    "For example, this figure shows the Graphviz output on the\n",
    "majority function in four variables:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F = Majority(a, b, c, d)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "%dotobj F"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Expression Parsing"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The `expr` function is a factory function that attempts to transform any\n",
    "input into a logic expression.\n",
    "It does the obvious thing when converting inputs that look like Boolean values:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "expr(False)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "expr(1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false,
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "expr(\"0\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "But it also implements a full top-down parser of expressions.\n",
    "For example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "expr(\"a | b ^ c & d\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "expr(\"s ? x[0] ^ x[1] : y[0] <=> y[1]\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "expr(\"a[0,1] & a[1,0] => y[0,1] | y[1,0]\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "See the [documentation](http://pyeda.readthedocs.org/en/latest/expr.html#from-the-expr-function)\n",
    "for a complete list of supported operators accepted by the `expr` function."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Satisfiability"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "One of the most interesting questions in computer science is whether a given\n",
    "Boolean function is satisfiable, or SAT.\n",
    "That is, for a given function $F$,\n",
    "is there a set of input assignments that will produce an output of $1$?"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "PyEDA Boolean functions implement two functions for this purpose,\n",
    "`satisfy_one`, and `satisfy_all`.\n",
    "The former answers the question in a yes/no fashion,\n",
    "returning a satisfying input point if the function is satisfiable,\n",
    "and `None` otherwise.\n",
    "The latter returns a generator that will iterate through all satisfying\n",
    "input points."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "SAT has all kinds of applications in both digital design and verification.\n",
    "In digital design, it can be used in equivalence checking,\n",
    "test pattern generation, model checking, formal verification,\n",
    "and constrained-random verification, among others.\n",
    "SAT finds its way into other areas as well.\n",
    "For example, modern package management systems such as apt and yum\n",
    "might use SAT to guarantee that certain dependencies are satisfied\n",
    "for a given configuration."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The `pyeda.boolalg.picosat` module provides an interface to the modern\n",
    "SAT solver PicoSAT.\n",
    "When a logic expression is in conjunctive normal form (CNF),\n",
    "calling the `satisfy_*` methods will invoke PicoSAT transparently.\n",
    "\n",
    "For example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F = OneHot(a, b, c)\n",
    "F.is_cnf()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F.satisfy_one()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "list(F.satisfy_all())"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "When an expression is not a CNF,\n",
    "PyEDA will resort to a standard, backtracking algorithm.\n",
    "The worst-case performance of this implementation is exponential,\n",
    "but is acceptable for many real-world scenarios."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Tseitin Transformation"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The worst case memory consumption when converting to CNF is exponential.\n",
    "This is due to the fact that distribution of $M$ `Or` clauses over\n",
    "$N$ `And` clauses (or vice-versa) requires $M \\times N$ clauses."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "Or(And(a, b), And(c, d)).to_cnf()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Logic expressions support the `tseitin` method,\n",
    "which perform's Tseitin's transformation on the input expression.\n",
    "For more information about this transformation, see (ref needed)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The Tseitin transformation does not produce an equivalent expression,\n",
    "but rather an *equisatisfiable* CNF,\n",
    "with the addition of auxiliary variables.\n",
    "The important feature is that it can convert any expression into a CNF,\n",
    "which can be solved using PicoSAT."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "F = Xor(a, b, c, d)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "soln = F.tseitin().satisfy_one()\n",
    "soln"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "You can safely discard the `aux` variables to get the solution:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "{k: v for k, v in soln.items() if k.name != 'aux'}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Truth Tables"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The most straightforward way to represent a Boolean function is to simply\n",
    "enumerate all possible mappings from input assignment to output values.\n",
    "This is known as a truth table,\n",
    "It is implemented as a packed list,\n",
    "where the index of the output value corresponds to the assignment of the\n",
    "input variables.\n",
    "The nature of this data structure implies an exponential size.\n",
    "For $N$ input variables, the table will be size $2^N$.\n",
    "It is therefore mostly useful for manual definition and inspection of\n",
    "functions of reasonable size."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To construct a truth table from scratch,\n",
    "use the `truthtable` factory function.\n",
    "For example, to represent the `And` function:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "truthtable([a, b], [False, False, False, True])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "# This also works\n",
    "truthtable([a, b], \"0001\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "You can also convert expressions to truth tables using the ``expr2truthtable`` function:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "expr2truthtable(OneHot0(a, b, c))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Partial Definitions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Another use for truth tables is the representation of *partially defined* functions.\n",
    "Logic expressions and binary decision diagrams are *completely defined*,\n",
    "meaning that their implementation imposes a complete mapping from all points\n",
    "in the domain to $\\{0, 1\\}$.\n",
    "Truth tables allow you to specify some function outputs as \"don't care\".\n",
    "You can accomplish this by using either `\"-\"` or `\"X\"` with the `truthtable` function.\n",
    "\n",
    "For example, a seven segment display is used to display decimal numbers.\n",
    "The codes \"0000\" through \"1001\" are used for 0-9,\n",
    "but codes \"1010\" through \"1111\" are not important, and therefore can be\n",
    "labeled as \"don't care\"."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "X = ttvars('x', 4)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "F1 = truthtable(X, \"0000011111------\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "F2 = truthtable(X, \"0001111100------\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To convert a table to a two-level,\n",
    "disjunctive normal form (DNF) expression,\n",
    "use the `truthtable2expr` function:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "truthtable2expr(F1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Two-Level Logic Minimization"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "When choosing a physical implementation for a Boolean function,\n",
    "the size of the logic network is proportional to its cost,\n",
    "in terms of area and power.\n",
    "Therefore it is desirable to reduce the size of that network."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Logic minimization of two-level forms is an NP-complete problem.\n",
    "It is equivalent to finding a minimal-cost set of subsets of a\n",
    "set $S$ that covers $S$.\n",
    "This is sometimes called the \"paving problem\",\n",
    "because it is conceptually similar to finding the cheapest configuration of\n",
    "tiles that cover a floor.\n",
    "Due to the complexity of this operation,\n",
    "PyEDA uses a C extension to the Berkeley Espresso library."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "After calling the `espresso_tts` function on the `F1` and `F2`\n",
    "truth tables from above,\n",
    "observe how much smaller (and therefore cheaper) the resulting DNF expression is:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "F1M, F2M = espresso_tts(F1, F2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F1M"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F2M"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Binary Decision Diagrams"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "A binary decision diagram is a directed acyclic graph used to represent a\n",
    "Boolean function.\n",
    "They were originally introduced by Lee,\n",
    "and later by Akers.\n",
    "In 1986, Randal Bryant introduced the reduced, ordered BDD (ROBDD).\n",
    "\n",
    "The ROBDD is a canonical form,\n",
    "which means that given an identical ordering of input variables,\n",
    "equivalent Boolean functions will always reduce to the same ROBDD.\n",
    "This is a desirable property for determining formal equivalence.\n",
    "Also, it means that unsatisfiable functions will be reduced to zero,\n",
    "making SAT/UNSAT calculations trivial.\n",
    "Due to these auspicious properties,\n",
    "the term BDD almost always refers to some minor variation of the ROBDD\n",
    "devised by Bryant.\n",
    "\n",
    "The downside of BDDs is that certain functions,\n",
    "no matter how cleverly you order their input variables,\n",
    "will result in an exponentially-sized graph data structure."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Construction"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Like logic expressions,\n",
    "you can construct a BDD by starting with symbolic variables\n",
    "and combining them with operators.\n",
    "\n",
    "For example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "a, b, c = map(bddvar, 'abc')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "F = a & b & c"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F.support"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F.restrict({a: 1, b: 1})"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F & 0"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The `expr2bdd` function can also be used to convert any expression into\n",
    "an equivalent BDD:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "expr2bdd(expr(\"(s ? d1 : d0) <=> (s & d1 | ~s & d0)\"))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Equivalence"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As we mentioned before,\n",
    "BDDs are a canonical form.\n",
    "This makes checking for SAT, UNSAT, and formal equivalence trivial."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "~a & a"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "~a & ~b | ~a & b | a & ~b | a & b"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "F = a ^ b"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "G = ~a & b | a & ~b"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F.equivalent(G)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F is G"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "PyEDA's BDD implementation uses a unique table,\n",
    "so `F` and `G` from the previous example are actually just two different\n",
    "names for the same object."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Visualization"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Like expressions,\n",
    "binary decision diagrams also support a `to_dot()` method,\n",
    "which can be used to convert the graph structure to DOT format\n",
    "for consumption by Graphviz.\n",
    "For example, this figure shows the Graphviz output on the\n",
    "majority function in three variables:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "%dotobj expr2bdd(expr(\"Majority(a, b, c)\"))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Function Arrays"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "When dealing with several related Boolean functions,\n",
    "it is usually convenient to index the inputs and outputs.\n",
    "For this purpose, PyEDA includes a multi-dimensional array (MDA) data type,\n",
    "called an `farray` (function array).\n",
    "\n",
    "The most pervasive example is computation involving any numeric data type.\n",
    "If these numbers are 32-bit integers, there are 64 total inputs,\n",
    "not including a carry-in.\n",
    "The conventional way of labeling the input variables is\n",
    "$a_0, a_1, \\ldots, a_{31}$, and $b_0, b_1, \\ldots, b_{31}$.\n",
    "\n",
    "Furthermore, you can extend the symbolic algebra of Boolean functions to arrays.\n",
    "For example, the element-wise XOR of `A` and `B` is also an array.\n",
    "\n",
    "In this section, we will briefly discuss `farray` construction,\n",
    "slicing operations, and algebraic operators.\n",
    "Function arrays can be constructed using any `Function` implementation,\n",
    "but for simplicity we will restrict the discussion to logic expressions."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Construction"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The `farray` constructor can be used to create an array of arbitrary expressions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "a, b, c, d = map(exprvar, 'abcd')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "F = farray([a, b, And(a, c), Or(b, d)])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F.ndim"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F.size"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "F.shape"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As you can see, this produces a one-dimensional array of size 4.\n",
    "\n",
    "The shape of the previous array uses Python's conventional,\n",
    "exclusive indexing scheme in one dimension.\n",
    "The `farray` constructor also supports multi-dimensional arrays:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "G = farray([ [a, b],\n",
    "             [And(a, c), Or(b, d)],\n",
    "             [Xor(b, c), Equal(c, d)] ])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "G.ndim"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "G.size"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "G.shape"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Though arrays can be constructed from arbitrary functions in arbitrary shapes,\n",
    "it is far more useful to start with arrays of variables and constants,\n",
    "and build more complex arrays from them using operators.\n",
    "\n",
    "To construct arrays of expression variables,\n",
    "use the `exprvars` factory function:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "xs = exprvars('x', 8)\n",
    "xs"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "ys = exprvars('y', 4, 4)\n",
    "ys"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Use the `uint2exprs` and `int2exprs` function to convert integers to their\n",
    "binary encoding in unsigned, and twos-complement, respectively."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "uint2exprs(42, 8)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "int2exprs(-42, 8)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Note that the bits are in order from LSB to MSB,\n",
    "so the conventional bitstring representation of $-42$ in eight bits\n",
    "would be \"11010110\"."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Slicing"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "PyEDA's function arrays support numpy-style slicing operators:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "xs = exprvars('x', 4, 4, 4)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "xs[1,2,3]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "xs[2,:,2]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "xs[...,1]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "A special feature of PyEDA `farray` slicing that is useful for digital logic\n",
    "is the ability to multiplex (mux) array items over a select input.\n",
    "For example, to create a simple, 4:1 mux:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "X = exprvars('x', 4)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "S = exprvars('s', 2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "X[S].simplify()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Algebraic Operations"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Function arrays are algebraic data types,\n",
    "which support the following symbolic operators:\n",
    "\n",
    "* unary reductions (`uor`, `uand`, `uxor`, ...)\n",
    "* bitwise logic (`~ | & ^`)\n",
    "* shifts (`<< >>`)\n",
    "* concatenation (`+`)\n",
    "* repetition (`*`)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Combining function and array operators allows us to implement a reasonably\n",
    "complete domain-specific language (DSL) for symbolic Boolean algebra in Python."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Consider, for example, the implementation of the `xtime` function,\n",
    "which is an integral part of the AES algorithm."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The Verilog implementation, as a `function`:\n",
    "\n",
    "```verilog\n",
    "   function automatic logic [7:0]\n",
    "   xtime(logic [7:0] b, int n);\n",
    "       xtime = b;\n",
    "       for (int i = 0; i < n; i++)\n",
    "           xtime = {xtime[6:0], 1'b0}\n",
    "                 ^ (8'h1b & {8{xtime[7]}});\n",
    "   endfunction\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "And the PyEDA implementation:\n",
    "\n",
    "```python\n",
    "  def xtime(b, n):\n",
    "       for _ in range(n):\n",
    "           b = (exprzeros(1) + b[:7]\n",
    "             ^  uint2exprs(0x1b, 8) & b[7]*8)\n",
    "       return b\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Practical Applications"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "Arrays of functions have many practical applications.\n",
    "For example,\n",
    "the `pyeda.logic.addition` module contains implementations of\n",
    "ripple-carry, brent-kung, and kogge-stone addition logic.\n",
    "Here is the digital logic implementation of $2 + 2 = 4$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "from pyeda.logic.addition import kogge_stone_add"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "A = exprvars('a', 8)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "B = exprvars('b', 8)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "S, C = kogge_stone_add(A, B)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "S.vrestrict({A: \"01000000\", B: \"01000000\"})"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.4.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 0
}
